The present disclosure relates to quality assurance of computerized systems in general, and to formal verification of computerized systems in particular.
Computerized devices are an important part of the modern life. Such devices control almost every aspect of our life—from writing documents to controlling traffic lights. However, computerized devices are bug-prone, and thus require a testing phase in which the bugs should be discovered. The testing phase is considered one of the most difficult tasks in developing a computerized device. Many developers of computerized devices invest a significant portion, sometimes as much as 70%, of the development cycle to discover erroneous behaviors of the computerized device, also referred to as a target computerized system. The target computerized system may comprise hardware, software, firmware, a combination thereof and the like.
During the testing phase, formal verification techniques may be applied to verify that a predetermined property is held. Formal verification may utilize a model checker to verify that the predetermined property is held. In some cases, a reference model is used in order to verify a model. The model may be designed by a chip designer, a software engineer or the like, and it represents the target computerized system, as designated to be produced. The model may comprise portions that are designed to increase efficiency or performance of the target computerized system, such as for example reducing power requirements, decreasing times a memory is accessed, using various storage devices such as a flash device in addition to a hard disk, accumulating data to a buffer before outputting the data and the like.